5.1 KB · ⇊ 4 parts · ⤓ Micron 5.1 KB · ⤓ HTML 17.0 KB

top

The Bernays–Schönfinkel class (also known as Bernays–Schönfinkel–Ramsey class) of formulas, named after Paul Bernays, Moses Schönfinkel and Frank P. Ramsey, is a fragment of first-order logic formulas where satisfiability is decidable.

It is the set of sentences that, when written in prenex normal form, have an ∃ ∃ ∗ ∗ ∀ ∀ ∗ ∗ {\displaystyle \exists ^{*}\forall ^{*}} quantifier prefix and do not contain any function symbols.

Ramsey proved that, if ϕ ϕ {\displaystyle \phi } is a formula in the Bernays–Schönfinkel class with one free variable, then either { x ∈ ∈ N : ϕ ϕ ( x ) } {\displaystyle \{x\in \mathbb {N} :\phi (x)\}} is finite, or { x ∈ ∈ N : ¬ ¬ ϕ ϕ ( x ) } {\displaystyle \{x\in \mathbb {N} :\neg \phi (x)\}} is finite.cite-ref-1[1]

This class of logic formulas is also sometimes referred as effectively propositional (EPR) since it can be effectively translated into propositional logic formulas by a process of grounding or instantiation.

The satisfiability problem for this class is NEXPTIME-complete.cite-ref-2[2]

• Applications

• See also

• Notes

• References

Efficient algorithms for deciding satisfiability of EPR have been integrated into SMT solvers.cite-ref-3[3]

• Prenex normal form

cite-note-11. ↑ citerefpratt-hartmann2023Pratt-Hartmann, Ian (2023-03-30). Fragments of First-Order Logic. Oxford University Press. p. 186. ISBN 978-0-19-196006-2.

cite-note-22. ↑ citereflewis1980Lewis, Harry R. (1980), "Complexity results for classes of quantificational formulas", Journal of Computer and System Sciences, 21 (3): 317–353, doi:10.1016/0022-0000(80)90027-6, MR 0603587

cite-note-33. ↑ citerefde-mourabj-rner2008de Moura, Leonardo; Bjørner, Nikolaj (2008). "Deciding Effectively Propositional Logic Using DPLL and Substitution Sets". In Armando, Alessandro; Baumgartner, Peter; Dowek, Gilles (eds.). Automated Reasoning. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer. pp. 410–425. doi:10.1007/978-3-540-71070-7_35. ISBN 978-3-540-71070-7.

• citereframsey1930Ramsey, F. (1930), "On a problem in formal logic", Proc. London Math. Soc., 30: 264–286, doi:10.1112/plms/s2-30.1.264

• citerefpiskacde-mourabjorner2008Piskac, R.; de Moura, L.; Bjorner, N. (December 2008), "Deciding Effectively Propositional Logic with Equality" (PDF), Microsoft Research Technical Report (2008–181)